COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 defini.lsp[w84,jmc]	EKL definition principle
C00004 00003	 An attempt to put the definitions in parametrized form
C00006 ENDMK
C⊗;
;;; defini.lsp[w84,jmc]	EKL definition principle

(decl par (type: |ground|))
(decl atc (type: |ground⊗ground→ground|))
(decl pairc (type:|ground⊗ground⊗ground⊗(ground→ground)⊗(ground→ground)→ground|))
(decl flat (type: |ground⊗ground→ground|))
(decl (f g) (type: |ground→ground|))

(axiom |∀atc pairc.
	(∃fun.(∀x y par.(atom x ⊃ fun(x,par) = atc(x,par))
∧ (fun(x.y,par) = pairc(x,y,par,λpar.fun(x,par),λpar.fun(y,par)))))|)
(label newsexpinductiondef)

(define flat
	|∀x y u.(atom x ⊃ flat(x,u) = x.u) ∧ (flat(x.y,u) = flat(x,flat(y,u)))|
	(use newsexpinductiondef
	     ue:
	     ((atc.|λx par.x.par|)
	      (pairc.|λ x y par f g.f(g(par))|))))

(decl (f g) (type: |(ground*) → (ground*)|))

(define flat
	|∀x y u.(atom x ⊃ flat(x,u) = x.u) ∧ (flat(x.y,u) = flat(x,flat(y,u)))|
	(use newsexpinductiondef1
	     ue:
	     ((atc1.|λx u.x.u|)
	      (pairc1.|λ x y u f g.f(g(u))|))))
;;; An attempt to put the definitions in parametrized form

(decl flat (type: |ground⊗ground→ground|))

(axiom |∀atc1 pairc1.
	(∃nfun.(∀x y pars.(atom x ⊃ nfun(x,pars) = atc1(x,pars))
∧ (nfun(x.y,pars) = pairc1(x,y,λpars.nfun(x,pars),λpars.nfun(y,pars),pars))))|)
(label newsexpinductiondef1)

(decl (f g) (type: |(ground*) → (ground*)|))

(define flat
	|∀x y u.(atom x ⊃ flat(x,u) = x.u) ∧ (flat(x.y,u) = flat(x,flat(y,u)))|
	(use newsexpinductiondef1
	     ue:
	     ((atc1.|λx u.x.u|)
	      (pairc1.|λ x y f g u.f(g(u))|))))

60. ;ATC1 is unknown.
;PAIRC1 is unknown.
;NFUN is unknown.
;the symbol NFUN declared to have type (GROUND⊗(GROUND*))→GROUND
;the symbol PAIRC1 declared to have type (GROUND⊗GROUND⊗((GROUND*)→GROUND)⊗((GROUND*)→GROUND)⊗(GROUND*))→GROUND
;the symbol ATC1 declared to have type (GROUND⊗(GROUND*))→GROUND
61. ;Labeled.
61. 
62. ;ue: λX Y F G U.F(G(U)) does not have the appropriate type.
62.